#include "RepeatedLiteralsRemover.cuh"

RepeatedLiteralsRemover::RepeatedLiteralsRemover(
		vector<Clause> & formula, int number_of_variables)
{
	this->formula = &formula;
	this->number_of_variables = number_of_variables;
	stats = (sat_status*) malloc(sizeof(sat_status)*number_of_variables);
	status = UNDEF;
}

RepeatedLiteralsRemover::~RepeatedLiteralsRemover()
{
	free(stats);
}

sat_status RepeatedLiteralsRemover::get_status()
{
	return status;
}

bool RepeatedLiteralsRemover::process_clause(Clause & clause)
{

	for(int i = 0; i < number_of_variables; i++)
	{
		stats[i] = UNDEF;
	}


	for(int i = 0; i < clause.number_of_lits; i++)
	{
		Var v = var(clause.literals[i]);
		bool s = sign(clause.literals[i]);
		sat_status stat = s ? SAT : UNSAT;

		if(stats[v] == UNDEF)
		{
			stats[v] = stat;
		}
		else
		{
			if(stats[v] == stat)
			{
				remove_literal(clause, i);
				i--;
			}
			else
			{
				return true;
			}
		}

	}
	return false;

}

void RepeatedLiteralsRemover::process()
{
	for(vector<Clause>::iterator it = formula->begin(); it != formula->end(); ++it)
	{
		bool must_remove = process_clause(*it);
		if(must_remove)
		{
			formula->erase(it);
			it--;
		}
	}

	status = formula->size() == 0 ? SAT : UNDEF;

}
